Nuprl Definition : R-icompat 11,40

R-icompat(A; B)
== if Rplus?(A)
== ifthen R-icompat(Rplus-left(A); B)  R-icompat(Rplus-right(A); B)
== if Rplus?(B)
== ifthen R-icompat(A; Rplus-left(B))  R-icompat(A; Rplus-right(B))
== if Rnone?(A)
== ifthen True
== if Rnone?(B)
== ifthen True
== if eq_id(R-loc(A); R-loc(B))
== ifthen True
== else R-interface-compat(A; B)  R-interface-compat(B; A)
== fi 
(recursive) 
latex


DefinitionsR-interface-compat(A; B), P  Q, True, R-loc(R), eq_id(a; b), if b then t else f fi , Rnone?(x1), Rplus-right(x1), f(a), Rplus-left(x1), Rplus?(x1), x.A(x), Y
FDL editor aliasesR-icompat

origin